#include <assert.h>
#include <iostream>
#include <stdlib.h>
#include <string.h>
#include "PrincessFormulaParser.h"


void PrincessFormulaParser::expect(const string& token) {
  if (nextToken != token)
    throw (string("Expected ") + token + " but received " + nextToken);
  computeNextToken();
}

void PrincessFormulaParser::consumeWhiteSpaces() {
  while (currentPos < charSeq.size() && charSeq[currentPos] == ' ')
    ++currentPos;
}

void PrincessFormulaParser::computeNextToken() {
  consumeWhiteSpaces();

  if (currentPos == charSeq.size()) {
    hasNextToken = false;
    nextToken = "EOF";
    return;
  }

  hasNextToken = true;

  switch (charSeq[currentPos]) {
  case '(': case ')':
    nextToken = charSeq[currentPos];
    ++currentPos;
    break;

  default:
    nextToken = "";
    do {
      nextToken += charSeq[currentPos];
      ++currentPos;
    } while (charSeq[currentPos] != '(' &&
         charSeq[currentPos] != ')' &&
         charSeq[currentPos] != ' ');
    break;
  }
}

Expr* PrincessFormulaParser::parseTerm(bool& untranslatable) {
  assert(hasNextToken);
  expect("(");
  //exprt res;
  Expr* exp;
  int i1;

  const string op = nextToken;
  computeNextToken();
  if (op == "+" || op == "*") {
    //res.id(op);
    //res.copy_to_operands(parseTerm(untranslatable));
    i1 = 0;
    exp = new BinExpr;
    if(op == "+"){
        ((BinExpr*)exp)->op = Plus;
    }
    else if(op == "*"){
        ((BinExpr*)exp)->op = Multi;
    }

    while (nextToken == "("){
      i1 = i1 + 1;
      if(i1 == 1){
          ((BinExpr*)exp)->e1 = parseTerm(untranslatable);
      }
      else if(i1 == 2){
          ((BinExpr*)exp)->e2 = parseTerm(untranslatable);
      }
      //res.copy_to_operands(parseTerm(untranslatable));
    }

  } else if (op == "sym") {
    //res.id("symbol");

    //PrincessLineariser::SymInfoMap::const_iterator pos =
    //  vocabulary.find(nextToken);
    //if (pos == vocabulary.end())
    //  throw (string("Expected an identifier, but received ") + nextToken);

    //res.set("identifier", pos->second.originalName);
    //res.set("type", pos->second.type);
    exp = new VarExpr;
    strcpy(((VarExpr*)exp)->x, nextToken.c_str());
    computeNextToken();
  } else if (op == "lit") {
    //res.id("constant");

    // the next token is an integer (not the binary representation)
    //res.set("value", nextToken);
    exp = new IntExpr;
    ((IntExpr*)exp)->i = atoi(nextToken.c_str());
    computeNextToken();
  } else if (op == "boundVar") {
    //res.id("boundVar");
    //res.set("identifier", nextToken);

    //boundVar are mathematical integers
    //res.set("type", "mathint");

    //quanStack.top().insert(res);
    exp = new VarExpr;
    strcpy(((VarExpr*)exp)->x, nextToken.c_str());
    quanStack.top().insert(exp);
    computeNextToken();

  } else if (op == "store") {
    // store is also used to represent structs so we need to differentiate

    //res.id("with");
    //res.copy_to_operands(parseTerm(untranslatable)); //old array or struct
    //res.copy_to_operands(parseTerm(untranslatable)); //index or member number
    //assert(res.op0().id()=="symbol");

    //if(res.op0().type().id()=="struct") {
      // member number has to be replaced with its name

      // member number must be a constant
      //mp_integer member_number;
      //const constant_exprt &const_expr = to_constant_expr(res.op1());
      //to_integer(const_expr, member_number);

      //const struct_typet &struct_type = to_struct_type(res.op0().type());
      //res.op1().id("member_name");
      //res.op1().set("component_name", struct_type.components()[integer2long(member_number)].get_name());
    //}

    //res.copy_to_operands(parseTerm(untranslatable)); // value

    //res.type()=res.op0().type();
    exp = new StoreExpr;
    ((StoreExpr*)exp)->a = parseTerm(untranslatable);
    ((StoreExpr*)exp)->i = parseTerm(untranslatable);
    ((StoreExpr*)exp)->e = parseTerm(untranslatable);

  } else if (op == "select") {
    // store is also used to represent structs so we need to differentiate

    //res.copy_to_operands(parseTerm(untranslatable)); // array or struct

    /*if (res.op0().type().id() == "") {
      // TODO: for now we assume that this select is for an array and not a struct.
      // this of course is not always the case but there is no obvious solution for now
      res.id("index");
      res.copy_to_operands(parseTerm(untranslatable)); // index
      untranslatable = true;
    } else if(res.op0().type().id()=="mathint") {
      //array has been quantified
      res.id("index");
      res.copy_to_operands(parseTerm(untranslatable)); // index
      res.type()=res.op0().type();

    } else if(res.op0().type().id()=="struct") {
      res.id("member");

      // parsing member number which must be a constant
      const constant_exprt const_expr = to_constant_expr(parseTerm(untranslatable));
      mp_integer member_number = string2integer(const_expr.get_string("value"));

      const struct_typet &struct_type = to_struct_type(res.op0().type());
      struct_union_typet::componentt component =
          struct_type.components()[integer2long(member_number)];
      res.set("component_name", component.get_name());

      assert(component.type().id()!="");
      res.type()=component.type();

    } else {
      res.id("index");
      res.copy_to_operands(parseTerm(untranslatable)); // index
      assert(res.op0().type().subtype().id()!="");
      res.type()=res.op0().type().subtype();
    }*/
    exp = new SelectExpr;
    //strcpy(((SelectExpr*)exp)->n, nextToken.c_str());
    ((SelectExpr*)exp)->a = parseTerm(untranslatable);
    ((SelectExpr*)exp)->i = parseTerm(untranslatable);
  }
  else {
    throw (string("Unknown operator: ") + op);
  }

  expect(")");
  return exp;
  //return res;
}

Prop* PrincessFormulaParser::parseFormula(int polarity) {
  //std::cout << charSeq << std::endl;
  //if(charSeq.compare("INVALID") == 0){ return NULL; }
  //if(charSeq.compare("VALID") == 0){ return NULL; }
  //cout << "charSeq = " << charSeq << endl;
  if(charSeq.compare("true") == 0){
      Prop* p;
      p = new BoolProp;
      ((BoolProp*)p)->b = true;
      return p;
  }
  assert(hasNextToken);

  expect("(");
  //exprt res;
  Prop* prop=NULL;

  const string op = nextToken;
  //const string op = "(= (f (lit 2) ) (lit 5) )";
  computeNextToken();
  if (op == "true" || op == "false") {
    prop = new BoolProp;
    if(op == "true"){
        ((BoolProp*)prop)->b = true;
    }
    else{
        ((BoolProp*)prop)->b = false;
    }
    //res.id("constant");
    //res.set("value", op);
  } else if (op == "=" || op == "<=" || op == ">=") {
    // some expressions might not be translatable ... in this
    // case we currently just replace the subformula with true/false
    bool untranslatable = false;

    if(op == "="){
        prop = new InequProp;
        ((InequProp*)prop)->e1 = parseTerm(untranslatable);
        ((InequProp*)prop)->e2 = parseTerm(untranslatable);
        ((InequProp*)prop)->p = Eq;
    }
    else if(op == "<="){
        prop = new NegProp;
        Prop *intermedia_prop;
        intermedia_prop = new InequProp;
        ((InequProp*)intermedia_prop)->e1 = parseTerm(untranslatable);
        ((InequProp*)intermedia_prop)->e2 = parseTerm(untranslatable);
        ((InequProp*)intermedia_prop)->p = GT;
        ((NegProp*)prop)->p = intermedia_prop;
    }
    else if(op == ">="){
        prop = new NegProp;
        Prop *intermedia_prop;
        intermedia_prop = new InequProp;
        ((InequProp*)intermedia_prop)->e1 = parseTerm(untranslatable);
        ((InequProp*)intermedia_prop)->e2 = parseTerm(untranslatable);
        ((InequProp*)intermedia_prop)->p = LT;
        ((NegProp*)prop)->p = intermedia_prop;
    }
    else{ }
    //const exprt left = parseTerm(untranslatable);
    //const exprt right = parseTerm(untranslatable);

    if (untranslatable) {
      //res.id("constant");
      //res.set("value", polarity > 0 ? "false" : "true");
    } else {
      //res.id(op);
      //res.copy_to_operands(left, right);
    }
  } else if (op == "&" || op == "|") {
    prop = new BinProp;
    ((BinProp*)prop)->p1 = parseFormula(polarity);
    ((BinProp*)prop)->p2 = parseFormula(polarity);
    if(op == "&"){
        ((BinProp*)prop)->l = And;
    }
    else if(op == "&"){
        ((BinProp*)prop)->l = Or;
    }
    //const exprt left = parseFormula(polarity);
    //const exprt right = parseFormula(polarity);

    //res.id(op == "&" ? "and" : "or");
    //res.copy_to_operands(left, right);
  } else if (op == "!") {
    prop = new NegProp;
    ((NegProp*)prop)->p = parseFormula(polarity);
    //const exprt sub = parseFormula(-polarity);

    //res.id("not");
    //res.copy_to_operands(sub);
  } else if(op == "exists" || op == "forall") {
    //(op == "exists")? res.id("exists") : res.id("forall");

    //exprt& qv = res.add_expr("qvars");
    //qv.id("qvars");
    prop = new QuantProp;
    if(op == "exists"){
        ((QuantProp*)prop)->t = Exist;
    }
    else if(op == "exists"){
        ((QuantProp*)prop)->t = Forall;
    }
    else{
    }

    quanStack.push(Quans());
    //const exprt formula = parseFormula(polarity);
    ((QuantProp*)prop)->p = parseFormula(polarity);

    for(Quans::const_iterator iter = quanStack.top().begin();
        iter != quanStack.top().end();
        iter++){
        (((QuantProp*)prop)->v_e).push_back(*iter);
      //qv.copy_to_operands(*iter);
    }

    quanStack.pop();

    //res.copy_to_operands(formula);
  } else {
    throw (string("Unknown boolean operator: ") + op);
  }

  //res.set("type", "bool");

  expect(")");
  return prop;
  //return res;
}
